((PRF3 (NIL . (DECL (X Y Z X1 X2 X3 Y1 Y2 Y3 Z1 Z2 Z3) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z3 .)) (Z1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z1 .)) (Y2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y2 .)) (X3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X3 .)) (X1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X1 .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 1 . SEXP .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X .)) (Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z .)) (X2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . X2 .)) (Y1 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y1 .)) (Y3 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Y3 .)) (Z2 . (VARIABLE . GROUND . SEXP . NIL . NIL . 1 . Z2 .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 1 .) (NIL . (DECL (A B C A1 A2 B1 B2 C1 C2) (OT& . GROUND) VARIABLE ATOM) . NIL . ((C2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C2 .)) (B2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B2 .)) (A2 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A2 .)) (C . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C .)) (A . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A .)) (ATOM . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . ATOM . PREFIX . 1000 .) . 2 . ATOM .)) (B . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B .)) (A1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . A1 .)) (B1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . B1 .)) (C1 . (VARIABLE . GROUND . ATOM . NIL . NIL . 2 . C1 .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 2 .) (NIL . (DECL (TT NNIL) (OT& . GROUND) CONSTANT ATOM) . NIL . ((NNIL . (CONSTANT . GROUND . ATOM . NIL . NIL . 3 . NNIL .)) (ATOM . 2) (TT . (CONSTANT . GROUND . ATOM . NIL . NIL . 3 . TT .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 3 .) (NIL . (DECL (G G1 G2 G3) (OT& . GROUND) VARIABLE) . NIL . ((G3 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G3 .)) (G1 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G1 .)) (G . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G .)) (G2 . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 4 . G2 .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 4 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 5 . CDR .)) (CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 5 . CAR .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 6 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 7 . PHI .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 7 .) ((((∀ G)) (⊃ (ATOM G) (SEXP G))) . (AXIOM (TM& ((∀ G)) (⊃ (ATOM G) (SEXP G)))) . NIL . ((SEXP . 1) (ATOM . 2) (G . 4)) . NIL . NIL . NIL . (8) . NIL . PRF3 . NIL . NIL . 8 .) ((((∀ X Y)) (SEXP (CONS X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (CONS X Y)))) . NIL . ((X . 1) (SEXP . 1) (Y . 1) (CONS . 6)) . NIL . NIL . NIL . (9) . NIL . PRF3 . NIL . NIL . 9 .) ((((∀ G)) (⊃ (SEXP G) (∨ (ATOM G) (((∃ X Y)) (= G (CONS X Y)))))) . (AXIOM (TM& ((∀ G)) (⊃ (SEXP G) (∨ (ATOM G) (((∃ X Y)) (= G (CONS X Y))))))) . NIL . ((X . 1) (SEXP . 1) (Y . 1) (ATOM . 2) (G . 4) (CONS . 6)) . NIL . NIL . NIL . (10) . NIL . PRF3 . NIL . NIL . 10 .) ((((∀ X Y)) (¬ (ATOM (CONS X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (CONS X Y))))) . NIL . ((X . 1) (Y . 1) (ATOM . 2) (CONS . 6)) . NIL . NIL . NIL . (11) . NIL . PRF3 . NIL . NIL . 11 .) ((((∀ X Y)) (= (CAR (CONS X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (CONS X Y)) X))) . NIL . ((X . 1) (Y . 1) (CAR . 5) (CONS . 6)) . NIL . NIL . NIL . (12) . NIL . PRF3 . NIL . NIL . 12 .) ((((∀ X Y)) (= (CDR (CONS X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (CONS X Y)) Y))) . NIL . ((X . 1) (Y . 1) (CDR . 5) (CONS . 6)) . NIL . NIL . NIL . (13) . NIL . PRF3 . NIL . NIL . 13 .) ((((∀ PHI A)) (∧ (PHI A) (((∀ X Y)) (⊃ (⊃ (∧ (PHI X) (PHI Y)) (PHI (CONS X Y))) (((∀ X)) (PHI X)))))) . (AXIOM (TM& ((∀ PHI)) (((∀ A)) (∧ (PHI A) (((∀ X Y)) (⊃ (⊃ (∧ (PHI X) (PHI Y)) (PHI (CONS X Y))) (((∀ X)) (PHI X)))))))) . NIL . ((X . 1) (Y . 1) (A . 2) (CONS . 6) (PHI . 7)) . NIL . NIL . NIL . (14) . NIL . PRF3 . NIL . NIL . 14 .) (NIL . (DECL (U V W U1 U2 U3 V1 V2 V3 W1 W2 W3) (OT& . GROUND) VARIABLE LIST) . NIL . ((W3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W3 .)) (W1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W1 .)) (V2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V2 .)) (U3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U3 .)) (U1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U1 .)) (V . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V .)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 15 . LIST .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U .)) (W . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W .)) (U2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . U2 .)) (V1 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V1 .)) (V3 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . V3 .)) (W2 . (VARIABLE . GROUND . LIST . NIL . NIL . 15 . W2 .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 15 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL)) . NIL . ((NULL . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 16 . NULL .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 16 .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NNIL . 3) (NULL . 16)) . NIL . NIL . NIL . (17) . NIL . PRF3 . NIL . NIL . 17 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((NNIL . 3) (U . 15) (NULL . 16)) . NIL . NIL . NIL . (18) . NIL . PRF3 . NIL . NIL . 18 .) ((LIST NNIL) . (AXIOM (TM& LIST NNIL)) . NIL . ((NNIL . 3) (LIST . 15)) . NIL . NIL . NIL . (19) . NIL . PRF3 . NIL . NIL . 19 .) ((((∀ G)) (⊃ (LIST G) (SEXP G))) . (AXIOM (TM& ((∀ G)) (⊃ (LIST G) (SEXP G)))) . NIL . ((SEXP . 1) (G . 4) (LIST . 15)) . NIL . NIL . NIL . (20) . NIL . PRF3 . NIL . NIL . 20 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((X . 1) (CONS . 6) (U . 15) (NULL . 16)) . NIL . NIL . NIL . (21) . NIL . PRF3 . NIL . NIL . 21 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (DECIDE (TM& ((∀ X U)) (= (CAR (CONS X U)) X)) (LR& 20 12)) . NIL . ((U . 15) (CONS . 6) (CAR . 5) (X . 1)) . NIL . NIL . NIL . (12 20) . NIL . PRF3 . NIL . NIL . 22 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (DECIDE (TM& ((∀ X U)) (= (CDR (CONS X U)) U)) (LR& 20 13)) . NIL . ((U . 15) (CONS . 6) (CDR . 5) (X . 1)) . NIL . NIL . NIL . (13 20) . NIL . PRF3 . NIL . NIL . 23 .) ((((∀ X U)) (LIST (CONS X U))) . (AXIOM (TM& ((∀ X U)) (LIST (CONS X U)))) . NIL . ((U . 15) (CONS . 6) (X . 1) (LIST . 15)) . NIL . NIL . NIL . (24) . NIL . PRF3 . NIL . NIL . 24 .) ((((∀ U)) (⊃ (¬ (NULL U)) (((∃ X U1)) (= U (CONS X U1))))) . (AXIOM (TM& ((∀ U)) (⊃ (¬ (NULL U)) (((∃ X U1)) (= U (CONS X U1)))))) . NIL . ((U . 15) (U1 . 15) (NULL . 16) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (25) . NIL . PRF3 . NIL . NIL . 25 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((X . 1) (NNIL . 3) (CONS . 6) (PHI . 7) (U . 15)) . NIL . NIL . NIL . (26) . NIL . PRF3 . NIL . NIL . 26 .) (NIL . (NAMERANGE LISTIND (LN& . 26)) . NIL . NIL . NIL . NIL . ((LISTIND 26)) . NIL . NIL . PRF3 . NIL . NIL . 27 .) (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT UNIVERSAL INFIX 990) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (1 . * . INFIX . 990 .) . 28 . * .))) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 28 .) ((((∀ V W)) (LIST (* V W))) . (AXIOM (TM& ((∀ V W)) (LIST (* V W)))) . NIL . ((W . 15) (LIST . 15) (V . 15) (* . 28)) . NIL . NIL . NIL . (29) . NIL . PRF3 . NIL . NIL . 29 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((NULL . 16) (U . 15) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28)) . NIL . NIL . NIL . (30) . NIL . PRF3 . NIL . NIL . 30 .) ((⊃ (LIST NNIL) (((∀ V)) (= (* NNIL V) (CONDI (NULL NNIL) V (CONS (CAR NNIL) (* (CDR NNIL) V)))))) . (∀E U (TM& . NNIL) (LN& . 30)) . NIL . ((NULL . 16) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28) (NNIL . 3) (LIST . 15)) . NIL . NIL . NIL . (30) . NIL . PRF3 . NIL . NIL . 31 .) ((((∀ V)) (= (* NNIL V) V)) . (REWRITE SIMPLIFY (LN& . 31) (LR& 17 19)) . NIL . ((V . 15) (* . 28) (NNIL . 3)) . NIL . NIL . NIL . (30 17 19) . NIL . PRF3 . NIL . NIL . 32 .) ((⊃ (∧ ((((λ U)) (= (* (* U V) W) (* U (* V W)))) NNIL) (((∀ X U)) (⊃ (= (* (* U V) W) (* U (* V W))) ((((λ U)) (= (* (* U V) W) (* U (* V W)))) (CONS X U))))) (((∀ U)) (= (* (* U V) W) (* U (* V W))))) . (∀E PHI (TM& ((λ U)) (= (* (* U V) W) (* U (* V W)))) (LN& . 26)) . NIL . ((X . 1) (NNIL . 3) (CONS . 6) (U . 15) (V . 15) (* . 28) (W . 15)) . NIL . NIL . NIL . (26) . NIL . PRF3 . NIL . NIL . 33 .) ((⊃ (∧ (LIST (CONS X U)) (LIST NNIL)) (⊃ (∧ (= (* (* NNIL V) W) (* NNIL (* V W))) (((∀ X U)) (⊃ (= (* (* U V) W) (* U (* V W))) (= (* (* (CONS X U) V) W) (* (CONS X U) (* V W)))))) (((∀ U)) (= (* (* U V) W) (* U (* V W)))))) . (λE T (LN& . 33)) . NIL . ((X . 1) (NNIL . 3) (CONS . 6) (U . 15) (V . 15) (* . 28) (W . 15) (LIST . 15)) . NIL . NIL . NIL . (26) . NIL . PRF3 . NIL . NIL . 34 .) ((⊃ (∧ (= (* (* NNIL V) W) (* NNIL (* V W))) (((∀ X U)) (⊃ (= (* (* U V) W) (* U (* V W))) (= (* (* (CONS X U) V) W) (* (CONS X U) (* V W)))))) (((∀ U)) (= (* (* U V) W) (* U (* V W))))) . (REWRITE SIMPLIFY (LN& . 34) (LR& 19 24)) . NIL . ((X . 1) (NNIL . 3) (CONS . 6) (U . 15) (V . 15) (* . 28) (W . 15)) . NIL . NIL . NIL . (26 19 24) . NIL . PRF3 . NIL . NIL . 35 .) ((⊃ (LIST (* V W)) (= (* NNIL (* V W)) (* V W))) . (∀E V (TM& * V W) (LN& . 32)) . NIL . ((V . 15) (* . 28) (NNIL . 3) (LIST . 15) (W . 15)) . NIL . NIL . NIL . (30 17 19) . NIL . PRF3 . NIL . NIL . 36 .) ((= (* NNIL (* V W)) (* V W)) . (REWRITE SIMPLIFY (LN& . 36) (LR& 29)) . NIL . ((V . 15) (* . 28) (NNIL . 3) (W . 15)) . NIL . NIL . NIL . (30 17 19 29) . NIL . PRF3 . NIL . NIL . 37 .) ((⊃ (((∀ X U)) (⊃ (= (* (* U V) W) (* U (* V W))) (= (* (* (CONS X U) V) W) (* (CONS X U) (* V W))))) (((∀ U)) (= (* (* U V) W) (* U (* V W))))) . (REWRITE SIMPLIFY (LN& . 35) (LR& 32 37)) . NIL . ((X . 1) (CONS . 6) (U . 15) (V . 15) (* . 28) (W . 15)) . NIL . NIL . NIL . (26 24 30 17 19 29) . NIL . PRF3 . NIL . NIL . 38 .) ((= (* (* (CONS X U) V) W) (* (* (CONS X U) V) W)) . (DECIDE (TM& = (* (* (CONS X U) V) W) (* (* (CONS X U) V) W))) . NIL . ((W . 15) (* . 28) (V . 15) (U . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . NIL . NIL . PRF3 . NIL . NIL . 39 .) ((((∀ V)) (= (* (CONS X U) V) (CONDI (NULL (CONS X U)) V (CONS (CAR (CONS X U)) (* (CDR (CONS X U)) V))))) . (∀E U (TM& CONS X U) (LN& . 30) (LR& 24)) . NIL . ((NULL . 16) (U . 15) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28) (X . 1)) . NIL . NIL . NIL . (30 24) . NIL . PRF3 . NIL . NIL . 40 .) ((((∀ V)) (= (* (CONS X U) V) (CONS X (* U V)))) . (REWRITE SIMPLIFY (LN& . 40) (LR& 21 22 23)) . NIL . ((U . 15) (V . 15) (CONS . 6) (* . 28) (X . 1)) . NIL . NIL . NIL . (30 24 21 12 13 20) . NIL . PRF3 . NIL . NIL . 41 .) ((= (* (* (CONS X U) V) W) (* (CONS X (* U V)) W)) . (SREWRITE RIGHT 2#1 (LN& . 39) (LR& 41)) . NIL . ((W . 15) (* . 28) (V . 15) (U . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (30 24 21 12 13 20) . NIL . PRF3 . NIL . NIL . 42 .) ((((∀ V4)) (= (* (CONS X (* U V)) V4) (CONDI (NULL (CONS X (* U V))) V4 (CONS (CAR (CONS X (* U V))) (* (CDR (CONS X (* U V))) V4))))) . (∀E U (TM& CONS X (* U V)) (LN& . 30) (LR& 24)) . NIL . ((NULL . 16) (U . 15) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28) (X . 1) (V4 . (VARIABLE . GROUND . LIST . NIL . NIL . 43 . V4 .))) . NIL . NIL . NIL . (30 24) . NIL . PRF3 . NIL . NIL . 43 .) ((= (* (CONS X (* U V)) W) (CONDI (NULL (CONS X (* U V))) W (CONS (CAR (CONS X (* U V))) (* (CDR (CONS X (* U V))) W)))) . (E∀E (QUOTE ((U TM& CONS X (* U V)) (V TM& . W))) (QUOTE (LN& . 30)) (QUOTE (LR& 24)) (QUOTE (LR&))) . NIL . ((NULL . 16) (U . 15) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28) (X . 1) (W . 15)) . NIL . NIL . NIL . (30 24) . NIL . PRF3 . NIL . NIL . 44 .) ((= (* (CONS X (* U V)) W) (CONS X (* (* U V) W))) . (SREWRITE SIMPLIFY 2 (LN& . 44) (LR& 21 22 23) (LR& 29)) . NIL . ((U . 15) (V . 15) (CONS . 6) (* . 28) (X . 1) (W . 15)) . NIL . NIL . NIL . (30 24 21 12 13 20 29) . NIL . PRF3 . NIL . NIL . 45 .) ((= (* (* (CONS X U) V) W) (CONS X (* (* U V) W))) . (SREWRITE RIGHT 2 (LN& . 39) (LR& 41 45)) . NIL . ((W . 15) (* . 28) (V . 15) (U . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (30 24 21 12 13 20 29) . NIL . PRF3 . NIL . NIL . 46 .) ((= (* (CONS X U) (* V W)) (CONDI (NULL (CONS X U)) (* V W) (CONS (CAR (CONS X U)) (* (CDR (CONS X U)) (* V W))))) . (E∀E (QUOTE ((U TM& CONS X U) (V TM& * V W))) (QUOTE (LN& . 30)) (QUOTE (LR& 24 29)) (QUOTE (LR&))) . NIL . ((NULL . 16) (U . 15) (V . 15) (CONS . 6) (CAR . 5) (CDR . 5) (* . 28) (X . 1) (W . 15)) . NIL . NIL . NIL . (30 24 29) . NIL . PRF3 . NIL . NIL . 47 .) ((= (* (CONS X U) (* V W)) (CONS X (* U (* V W)))) . (SREWRITE SIMPLIFY 2 (LN& . 47) (LR& 21 22 23) (LR& 29)) . NIL . ((U . 15) (V . 15) (CONS . 6) (* . 28) (X . 1) (W . 15)) . NIL . NIL . NIL . (30 24 21 12 13 20 29) . NIL . PRF3 . NIL . NIL . 48 .) ((= (* (* U V) W) (* U (* V W))) . (ASSUME (TM& = (* (* U V) W) (* U (* V W)))) . NIL . ((U . 15) (V . 15) (* . 28) (W . 15)) . NIL . NIL . NIL . (49) . NIL . PRF3 . NIL . NIL . 49 .) ((= (* (* (CONS X U) V) W) (CONS X (* U (* V W)))) . (REWRITE RIGHT (LN& . 46) (LR& 49)) . NIL . ((W . 15) (* . 28) (V . 15) (U . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (30 24 21 12 13 20 29 49) . NIL . PRF3 . NIL . NIL . 50 .) ((= (* (* (CONS X U) V) W) (* (CONS X U) (* V W))) . (SREWRITE LEFT 2 (LN& . 50) (LR& 48)) . NIL . ((W . 15) (* . 28) (V . 15) (U . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (49 30 24 21 12 13 20 29) . NIL . PRF3 . NIL . NIL . 51 .) ((⊃ (= (* (* U V) W) (* U (* V W))) (= (* (* (CONS X U) V) W) (* (CONS X U) (* V W)))) . (⊃I (LN& . 49) (LN& . 51)) . NIL . ((U . 15) (V . 15) (* . 28) (W . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (29 20 13 12 21 24 30) . NIL . PRF3 . NIL . NIL . 52 .) ((((∀ X U)) (⊃ (= (* (* U V) W) (* U (* V W))) (= (* (* (CONS X U) V) W) (* (CONS X U) (* V W))))) . (∀I (X U) (LN& . 52)) . NIL . ((U . 15) (V . 15) (* . 28) (W . 15) (CONS . 6) (X . 1)) . NIL . NIL . NIL . (29 20 13 12 21 24 30) . NIL . PRF3 . NIL . NIL . 53 .) ((((∀ U)) (= (* (* U V) W) (* U (* V W)))) . (⊃E (LN& . 53) (LN& . 38)) . NIL . ((U . 15) (V . 15) (* . 28) (W . 15)) . NIL . NIL . NIL . (20 13 12 21 26 24 30 17 19 29) . NIL . PRF3 . NIL . NIL . 54 .)))